OpenPublicPlusTypeError.agda:12,17-21
Set₂ != Set
when checking that the expression Set₁ has type Set
